Nuprl Lemma : fadd_increasing
4,23
postcript
pdf
n
:
,
f
,
g
:(
n
). increasing(
f
;
n
)
nondecreasing(
g
;
n
)
increasing(fadd(
f
;
g
);
n
)
latex
Definitions
nondecreasing(
f
;
k
)
,
fadd(
f
;
g
)
,
increasing(
f
;
k
)
,
,
i
j
<
k
,
P
&
Q
,
A
B
,
A
,
False
,
P
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
{
i
..
j
}
Lemmas
le
wf
,
nat
wf
,
int
seg
wf
origin
n:
, f, g:(n
). increasing(f;n) 
nondecreasing(g;n) increasing(fadd(f;g);n) n:, f, g:(n). increasing(f;n) nondecreasing(g;n) increasing(fadd(f;g);n) 
j < kB
A Qx:A. B(x)
T
}